forall a: forall b:
forall Q:a->b:
I:a < Q;Q^ <=> 
Q;L:b,a = L:a